Skip to content

feat(ErdosProblems/114): add finite n <= 14 EHP certificate variant#3958

Open
bengoechea wants to merge 2 commits into
google-deepmind:mainfrom
MendozaLab:erdos-problem-114-v13-finite
Open

feat(ErdosProblems/114): add finite n <= 14 EHP certificate variant#3958
bengoechea wants to merge 2 commits into
google-deepmind:mainfrom
MendozaLab:erdos-problem-114-v13-finite

Conversation

@bengoechea
Copy link
Copy Markdown
Contributor

@bengoechea bengoechea commented May 8, 2026 •
edited
Loading

Summary

This adds Erdős Problem 114, the Erdős--Herzog--Piranian lemniscate-length conjecture.

The all-degree conjecture is stated as open. A separate finite-degree sibling statement records the current certificate-backed range 1 ≤ n ≤ 14:

  • n = 1: elementary translated-circle case
  • n = 2: MacLane / Eremenko--Hayman degree-two case
  • 3 ≤ n ≤ 14: Mendoza finite-degree IEEE-1788 interval certificate packet

The external certificate pipeline is not formalized in this Lean file, so the finite statement remains a sorry rather than being discharged by imported certificate axioms.

References

Notes

This supersedes the older #3712 approach. That branch encoded per-degree certificate conclusions as axioms; this PR instead keeps the finite result as an externally certificate-backed statement with a sorry, making the boundary between Lean formalization and external computation explicit.

Validation

  • Earlier clean-worktree validation: lake build FormalConjectures completed successfully before the DOI-version update.
  • DOI-version update commit 713d3fa: lake build FormalConjectures.ErdosProblems.«114» completed successfully.
  • A wording/proof-integrity scan found no imported certificate axioms and no claim that the all-degree conjecture is resolved.
  • DOI wording now cites version DOI 10.5281/zenodo.20087919 for the corrected v3.1.0 packet and concept DOI 10.5281/zenodo.19184467 for the latest-version family.

Issue

Closes #358

@bengoechea bengoechea mentioned this pull request May 8, 2026
Closed
@github-actions github-actions Bot added the erdos-problems Erdős Problems label May 8, 2026
@bengoechea
Copy link
Copy Markdown
Contributor Author

bengoechea commented May 8, 2026

Follow-up after the Zenodo manual version was published: commit 713d3fa updates the Lean reference to pin the corrected v3.1.0 certificate packet at version DOI 10.5281/zenodo.20087919, while keeping the concept DOI 10.5281/zenodo.19184467 for the latest-version family.

Targeted validation for this DOI-only commit: lake build FormalConjectures.ErdosProblems.«114» completed successfully in a clean PR worktree.

@Smetalo
Copy link
Copy Markdown
Contributor

Smetalo commented May 12, 2026

Does this resolve #358?

@bengoechea
Copy link
Copy Markdown
Contributor Author

bengoechea commented May 13, 2026

@Smetalo Yes, this PR formalizes the statement of Erdős Problem 114 tracked in #358, so merging should close that issue.

To be precise about what's formalized vs. proved:

  • erdos_114 (the all-degree Erdős–Herzog–Piranian conjecture) is stated with answer(sorry) — the underlying problem is still open, so this matches the repo's standard treatment of open conjectures.
    • The finite-degree sibling erdos_114.finite_le_14 records the certificate-backed range 1 ≤ n ≤ 14 (n=1 elementary, n=2 MacLane / Eremenko–Hayman, 3 ≤ n ≤ 14 via the external IEEE-1788 interval certificate packet, Zenodo v3.1.0 DOI 10.5281/zenodo.20087919). The certificate pipeline lives outside Lean, so this theorem also remains a sorry — the boundary between Lean formalization and external computation is explicit, no imported certificate axioms.
      So Erdős Problem 114: maximize length of curve of modulus one curve. #358 is resolved in the formalization sense (statement added to the corpus) but not in the mathematical sense (the conjecture remains open). Happy to add a Closes #358 line to the PR description if that's the project preference.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

erdos-problems Erdős Problems

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Erdős Problem 114: maximize length of curve of modulus one curve.

2 participants

@bengoechea @Smetalo